\begin{tabbing}
onceR\=\{\$a:ut2, \$done:ut2\}\+
\\[0ex]($i$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=[@$i$ \=precondition for "\$a"(v:Unit):\+\+
\\[0ex]$\lambda$$s$,$v$. $s$."\$done" $=$ false$_{2}$ $\in$ $\mathbb{B}$ State("\$done" : $\mathbb{B}$) v
\-\\[0ex]; @$i$ "\$done" initially false$_{2}$:$\mathbb{B}$
\\[0ex]; @$i$ effect locl("\$a")(v:Unit)  "\$done" := $\lambda$$s$,$v$. true$_{2}$ State("\$done" : $\mathbb{B}$) v 
\\[0ex]/ @$i$ only events in locl("\$a").nil change "\$done":$\mathbb{B}$.nil])
\-
\end{tabbing}